rtag(${\it info}$;$e$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Case ${\it info}$($e$) of inl($p$) $\Rightarrow$ $\cdot$ ; inr($q$) $\Rightarrow$ 2of($q$)